Nuprl Lemma : fpf-dom-compose
11,40
postcript
pdf
x
:Top,
f
:
a
:Top fp
Top,
g
,
eq
:Top.
x
dom(
g
o
f
) ~
x
dom(
f
)
latex
Definitions
Top
,
t
T
,
x
.
t
(
x
)
,
x
:
A
.
B
(
x
)
,
a
:
A
fp
B
(
a
)
,
fpf
dom
compose
compseq
tag
def
Lemmas
fpf
wf
,
top
wf
origin
x:Top, f:a:Top fp
Top, g, eq:Top. x 
dom(g o f) ~ x dom(f) x:Top, f:a:Top fp Top, g, eq:Top. x dom(g o f) ~ x dom(f) T
x. t(x)x:A. B(x) B(a)